package arlab.formulae

/**
 * Created by IntelliJ IDEA.
 * User: Eve
 * Date: 23.02.12
 * Time: 12:39
 * To change this template use File | Settings | File Templates.
 */

// boolsche Konstante für True
object Unification {
  
  def unifiable (tms: List[(Term, Term)]) : Boolean = unifyHelper(List(), tms)
  
  def unifyHelper(T:List[(Term,Term)], tms:List[(Term,Term)]):Boolean = if (tms.isEmpty)true else tms.head match{
    case (a,b)  if (a == b) =>  unifyHelper (T, tms.tail)
    case (a: Function, b: Function) if (a.name == b.name && a.terms.length == b.terms.length) =>
                unifyHelper(T, createNewTuples(List()++ a.terms, List()++ b.terms) ++ tms.tail)
    case (a: Function, b: Function) => false
    case (a:Variable, b) => (T.foldLeft(None:Option[Term]){(total, n) => if (n._1 == a) Some(n._2) else total}:Option[Term] ) match {
                                case Some(s) => unifyHelper(T, tms.tail :+ (s,b))
                                case None => if (testZycl (a,b)) false
                                             else unifyHelper(T :+ (a,b), tms.tail) 
                            }
    case (a, b:Variable) => unifyHelper(T, tms.tail :+ (b,a))
    case other => false    
  }
  
  def testZycl(a:Variable, b:Term):Boolean = b match {
        case b:Variable => a == b
        case b:Function => b.terms.foldLeft(false){(total, n) => total || testZycl(a,n)}
  }
  
  def createNewTuples (ls1: List[Term], ls2: List[Term]): List[(Term,  Term)] = 
    if (ls1.isEmpty) List()
    else createNewTuples (ls1.tail,  ls2.tail) :+ (ls1.head,  ls2.head)

  
  def unifyPredicate(tms:List[(Formula, Formula)]):Boolean = if (tms.isEmpty) true else tms.head match{
    case (a,b) if (a == b) => unifyPredicate (tms.tail)
    case (a: Predicate, b:Predicate) if (a.name == b.name && unifiable(createNewTuples(List() ++ a.terms, List() ++ b.terms))) => unifyPredicate(tms.tail) 

    case (a: Not, b: Not) => unifyPredicate(tms.tail :+ (a.a, b.a))  
    case other => false
  }
}
